Đi theo cách tiếp cận của Tóth, Thomas Hales, người sau đó làm việc tại Đại học Michigan, đã xác định rằng mật độ lớn nhất của tất cả các sắp xếp có thể được tính ra bằng việc tối thiểu hóa một công thức với 150 biến. Vào năm 1992, với sự hỗ trợ của học trò Samuel Ferguson, Hales giải quyết vấn đề trên chương tình tìm kiếm để ứng dụng có hệ thống quy hoạch tuyến tính để tìm các giá trị nhỏ hơn của giá trị của một công thức, cho mỗi tập hợp của hơn 1500 cấu hình khác nhau của các quả cầu. Nếu giá trị thấp hơn (so với giá trị của công thức) có thể được tìm thấy cho mọi tập hợp của những cấu hình tốt hơn giá trị của công thức cho sự sắp xếp khối lập phương, giả thiết Kepler sẽ được chứng minh. Để tìm giá trị nhỏ hơn cho tất cả các trường hợp, cần phải giải quyết tầm khoảng 100,000 vấn đề quy hoạch tuyến tính.

Khi giới thiệu quá trình thực hiện chương trình vào năm 1996, Hales nói rằng cái kết vẫn còn ở phía trước, nhưng có thể chỉ cần "một đến hai năm" là giải quyết được. Vào tháng 8 năm 1998, Hales đã tuyên bố giả thuyết đã được chứng minh. Vào thời điểm đó, chứng minh gồm 250 trang của ghi chú và 3 gigabyte của chương trình máy tính, dữ liệu và kết quả.

Mặc cho sự thiết tự nhiên của phương pháp, biên tập viên của Annals of Mathematics đã đồng ý xuất bản nó, cung cấp rằng nó được chấp nhận bởi 20 người đứng ra làm trọng tài. Vào năm 2003, sau sự xuất bản đó 4 năm, người đứng đầu của ban trọng tài lúc đó, Gábor Fejes Tóth, đã tuyên bố phương pháp được xác định 99% là chính xác, nhưng có thể nó không được chứng nhận sự chính xác của tất cả các tính toán máy tính.

Sau đó, vào năm 2005, Hales đã xuất bản tài liệu gồm 100 trang mô tả chi tiết phần không được thực hiện bằng máy tính của chứng minh của ông. Vào năm 2006, cả Hales và Ferguson đã cho xuất bản một tài liệu khác, cùng với đó là các tài liệu tiếp theo mô tả phần máy tính thực hiện của chứng minh. Cuối cùng, cả Hales và Ferguson nhận Giải Fulkerson vào năm 2009 cho việc giải quyết các vấn đề toán học không cần giấy tờ.

Chứng minh chính thức

Vào tháng 1 năm 2003, Hales đã tuyên bố một dự án hợp tác để cho ra đời phương pháp chứng minh hoàn thiện cho giả thuyết Kepler. Mục tiêu là loại bỏ bất kỳ sự không chắc chắn về khả năng đúng đắn của chứng minh bằng việc xây dựng một chứng minh chính thức có thể được xác minh bằng kiểm tra chứng minh tự động như các phần mềm HOL Light và Isabelle. Dự án mang tên Flyspeck, các chữ F, P và K là viết tắt của Former Proof of Kepler (Chứng minh chính thức của Kepler). Hales ước tính việc đưa ra một chứng minh chính thức hoàn toàn có thể mất khoảng 20 năm. Hales lần đầu xuất bản một bản thiết kế cho chứng minh chính thức vào năm 2012,[4] dự án được tuyên bố đã hoàn thành vào ngày 10 tháng 8 năm 2014[5]. Vào tháng 1 năm 2015, Hales và 21 cộng sự đã nộp một tài liệu mang tên Chứng minh chính thức cho giả thiết Kepler cho arXiv, tuyên bố rằng đã chứng minh được giả thiết[6]. Vào năm 2017, phương pháp chính thức đã được chấp nhận bởi tạp chí Forum of Mathematics.[1]